(*
  Timer Module
*)

Require Import base.

Require Import Classical.
Require Import Omega.
Require Import arithsimp.
Require Import logicsimp.

Module Type TimerInputSig.
  Parameter IN : tpBvar.
  Parameter PT : tpNvar.
  Parameter Q  : tpBvar.   (* main output.  *)
End TimerInputSig.

(* Timer generation functor. *)

Module TimerGen (X:TimerInputSig).

  (* input variables *)
  Definition IN := X.IN.  (* input enable. *)
  Definition PT := X.PT.  (* preset time.  *)

  (* output variable *)
  Definition Q  := X.Q.   (* main output.  *)
  Parameter  ET : tpNvar.   (* elapsed time. *)

(* elapsed time reset. *)
Axiom timer_ET_reset : 
  forall t, ~(IN t) -> (ET (S t) = 0). 
  
(* elapsed time increment. *)
Axiom timer_ET_inc : 
  forall t, (IN t) /\ (ET t) < (PT t) -> (ET (S t) = S (ET t)). 

(* elapsed time maintained. *)
Axiom timer_ET_maintain : 
  forall t, (IN t) /\ (ET t) = (PT t) -> (ET (S t) = (ET t)). 

(* main output. *)
Axiom timer_Q : 
  forall t, Q (S t) = (((ET t) = (PT t)) /\ (IN t)).

(* n keeps constant in [t1,t2]. *)
Definition nat_const (A:Type) (v:nat->A) (t1:nat) (t2:nat) :=
  forall t, close_close t1 t t2 -> (v t = v t1).

Implicit Arguments nat_const [A].

Definition PT_const t1 t2 := nat_const PT t1 t2.

(* if n is constant in [t1,t2], then it is constant in its sub interval. *)
Lemma nat_const_small : forall (A:Type) (n:nat->A) t1 t2 t3 t4,
  nat_const n t1 t2 -> t1<=t3 -> t4 <= t2 ->
  nat_const n t3 t4.
Proof.
unfold nat_const in |- *; intros.
rewrite (H t) in |- *.
 rewrite (H t3) in |- *.
  trivial.
 unfold close_close in |- *; unfold close_close in H2;  omega.
unfold close_close in |- *; unfold close_close in H2;  omega.
Qed.

(* constant keep same values at any two points within the region. *)
Lemma duration_constant :
  forall (n:tpNvar) t1 t2 t3 d, 
    t1<=t3 -> t3+d <= t2 -> 
    nat_const n t1 t2 -> (n t3 = n (t3+d)).
Proof.
intros; unfold nat_const in H1.
assert (n t3 = n t1).
 apply H1.
   unfold close_close in |- *;  omega.
assert (n (t3 + d) = n t1).
 apply H1; unfold close_close in |- *;  omega.
 omega.
Qed.

Lemma interval_constant :
  forall (n:tpNvar) t1 t2 t3 t4, 
    t1<=t3 -> t3<=t4 -> t4 <= t2 -> 
    nat_const n t1 t2 -> (n t3 = n t4).
Proof.
intros; unfold nat_const in H1.
unfold nat_const in H2.
assert (n t3 = n t1).
 apply H2; unfold close_close in |- *;  omega.
assert (n t4 = n t1).
 apply H2; unfold close_close in |- *;  omega.
 omega.
Qed.

  
(* In the specified durating, if PT is constant, then ET is always less than PT. *)
Lemma ET_limit_duration : 
  forall t1 d, (ET t1) <= (PT t1) ->
  (nat_const PT t1 (t1+d)) ->
  (forall t, t<=d -> (ET (t1+t)) <= (PT (t1+t))).
Proof.
induction t.
 intro;  autorewrite with arith_simp; assumption.
assert (IN (t1 + t) \/ ~ IN (t1 + t)); [ apply classic | idtac ].
  intro.
  assert (PT (t1 + t) = PT (t1 + S t)).
 apply (interval_constant PT t1 (t1 + d) (t1 + t) (t1 + S t)); try  omega.
   assumption.
rewrite <- H3 in |- *.
  case H1.
 intro.
   rewrite plus_SR in |- *.
   Split_less_than IHt; try intro.
  rewrite timer_ET_inc in |- *.
    omega.
   tauto.
 rewrite timer_ET_maintain in |- *.
   omega.
 auto.
  omega.
intro.
  rewrite plus_SR in |- *.
  rewrite timer_ET_reset in |- *.
  omega.
assumption.
Qed.
    

(* In the specified durating, if PT is constant, then ET is always less than PT. *)
Lemma ET_limit_interval : forall t1 t2, 
  (ET t1) <= (PT t1) ->
  (nat_const PT t1 t2) ->  
  (forall t, close_close t1 t t2 -> (ET t) <= (PT t)).
Proof.
intros t1 t2 H1 H2.
intros.
assert (exists t' : _, t2 = t1 + t').
 exists (t2 - t1).
   unfold close_close in H;  omega.
generalize H.
  elim H0.
  intro x.
  intro Ht2.
  rewrite Ht2 in |- *.
  generalize t.
  apply imply_close_close.
  apply ET_limit_duration.
 assumption.
rewrite <- Ht2 in |- *; assumption.
Qed.

(* ET will not decrease when PT and IN kept constant. *)
Lemma ET_monotonicity : 
  forall t,
    ET t <= PT t -> IN t ->
    PT (S t) = PT t -> IN (S t) = IN t ->
    ET t <= ET (S t).
Proof.
intros.
 Split_less_than H.
  rewrite timer_ET_inc in |- *; try  omega || auto.
 rewrite timer_ET_maintain in |- *; try  omega || auto.
Qed.

(* if PT and IN are constant, then ET will increase from 0 such that ET t = t. *)
Lemma timer_ET_increase : 
  let c := PT 0 in
  (ET 0 = 0) -> IN 0 -> 
  (nat_const PT 0 c) -> (nat_const (A:=Prop) IN 0 c) ->
  forall t, t <= c -> (ET t = t).
Proof.
induction t.
  omega.
intro.
  assert (ET t < PT t).
 rewrite IHt in |- *.
  unfold nat_const in H1.
    rewrite H1 in |- *.
   unfold c in H3.
      omega.
  unfold close_close in |- *;  omega.
  omega.
rewrite timer_ET_inc in |- *; try  omega.
  split.
 rewrite H2 in |- *.
  assumption.
 unfold close_close in |- *;  omega.
assumption.
Qed.

Lemma timer_ET_value : 
  forall t0, let c := PT t0 in
  (ET t0 = 0) -> IN t0 -> 
  (nat_const PT t0 (t0+c)) -> 
  (nat_const (A:=Prop) IN t0 (t0+c)) ->
  forall t, t <= c -> (ET (t0+t) = t).
Proof.
induction t.
  autorewrite with arith_simp;  omega.
intro.
  assert (ET (t0 + t) < PT (t0 + t)).
 rewrite IHt in |- *.
  unfold nat_const in H1.
    rewrite H1 in |- *.
   unfold c in H3.
      omega.
  unfold close_close in |- *;  omega.
  omega.
rewrite plus_SR in |- *.
  rewrite timer_ET_inc in |- *.
 f_equal.
   apply IHt;  omega.
split.
 rewrite H2 in |- *; auto.
   unfold close_close in |- *;  omega.
assumption.
Qed.

(* timer elapsed time will reach PT after PT scans. *)
Lemma timer_ET_main : 
  forall t, let c := PT t in
  (ET t = 0) -> IN t -> 
  (nat_const PT t (t+c)) -> 
  (nat_const (A:=Prop) IN t (t+c)) ->
  ((ET (t+c)) = c).
Proof.
  intros; apply timer_ET_value;  auto.
Qed.

(* trigger the main output. *)
Theorem timer_Q_main :
  forall t, let c := PT t in
  (ET t = 0) -> IN t -> 
  (nat_const PT t (t+c)) -> 
  (nat_const (A:=Prop) IN t (t+c)) ->
  Q (S(t+c)).
Proof.
intros.
assert (ET (t + c) = c).
 unfold c in |- *.
   apply timer_ET_main; auto.
rewrite timer_Q in |- *.
  split.
 rewrite H3 in |- *.
   rewrite H1 in |- *.
  auto.
 unfold close_close in |- *;  omega.
rewrite H2 in |- *; auto.
  unfold close_close in |- *;  omega.
Qed.

(* Q = false before the preset time c. *)
Theorem timer_notQ_main :
  forall t, let c := PT t in
  (ET t = 0) -> IN t -> ~(Q t) ->
  (nat_const PT t (t+c)) -> 
  (nat_const (A:=Prop) IN t (t+c)) ->
  (forall t', t' < c -> ~(Q (S(t+t')))).
Proof.
  intros.
  rewrite timer_Q; Logic_simplify; left.
  (* ET (t + t') <> PT (t + t') *)
assert (ET (t + t') = t').
 apply timer_ET_value; auto.
   unfold c in H4;  omega.
rewrite H5 in |- *.
  unfold nat_const in H2.
  assert (PT (t + t') = PT t).
 rewrite (H2 (t + t')) in |- *; trivial.
   unfold close_close in |- *;  omega.
rewrite H6 in |- *; unfold c in H4;  omega.
Qed.

End TimerGen.
